home *** CD-ROM | disk | FTP | other *** search
/ Language/OS - Multiplatform Resource Library / LANGUAGE OS.iso / quintus / quintus0.lha / work / command_2.06.2 < prev    next >
Text File  |  1992-04-03  |  17KB  |  382 lines
  1. %%% COMMANDS 
  2. %%% version 2.00.0 (based on command_19.4)
  3. %%%   added equality transformation
  4. %%% version 2.00.1
  5. %%%   added equality rewriting
  6. %%% version 2.00.3
  7. %%%   changed "equality_rewriting" to "auto_orient"
  8. %%%   added "outrwr", added "outrwt", added "outtreq", and "pullout_constants"
  9. %%% version 2.00.6
  10. %%%   added "include_original_clause"
  11. %%%   changed default of "simple_small_proof_check" from clear to set
  12. %%% version 2.00.8
  13. %%%   added lexicographic path ordering
  14. %%% version 2.03.4
  15. %%%   incorporated changes made to clin V1 between 7/31/90 and 10/18/90 which
  16. %%%     are visible externally -- changes to comments, predicate names, and
  17. %%%     variable names are not incorporated
  18. %%%   made "outrwr", "outrwt", and "outtreq" default to clear
  19. %%% version 2.03.6
  20. %%%   increased number of variables allowed in clauses from 20 to 100
  21. %%% version 2.04.3
  22. %%%   changed pullout_constants default value to clear
  23. %%% version 2.04.5
  24. %%%   added restricted_rewrite to control whether restricted or unrestricted
  25. %%%     rewriting of equations is used
  26. %%%   added equality_transform_each_round flag
  27. %%%   added safe_early_priority_test flag
  28. %%%   added early_unit_subsumption flag
  29. %%%   added early tautology test
  30. %%%   added small_proof_nucleus_bound
  31. %%%   corrected setting of paramters with infinity default
  32. %%% version 2.04.6
  33. %%%   added fixed_priority
  34. %%%   added start_priority_bound
  35. %%% version 2.04.8
  36. %%%   added group_detection
  37. %%% version 2.05.1
  38. %%%   added clause splitting
  39. %%% version 2.05.5
  40. %%%   added equational rewriting
  41. %%% version 2.05.6
  42. %%%   changed early unit subsumption to equality early unit subsumption
  43. %%%   added new early unit subsumption
  44. %%% version 2.05.8
  45. %%%   renamed assign/2 to assign_cmd/2 for compatibility with Quintus Prolog 3
  46. %%%   added priority_bound_increment
  47. %%% version 2.06.0
  48. %%%   added clause_generation_loop flag
  49. %%%   added save_rewrite_rules
  50. %%% version 2.06.1
  51. %%%   added constrained rewriting
  52. %%%   added save_unrestricted_normal_form
  53. %%% version 2.06.2
  54. %%%   added fast_priority_update
  55. %%%   added duplicate_partial_instance_test
  56. %%%   added precompute_constraints
  57. %%%   added restricted_equality_transform
  58. %%%   added cache_size
  59. %%%   changed restricted_equality_transform default to 0
  60. %%%
  61. %%% This file contains a list of settings. Commands for setting and
  62. %%% retracting settings are also provided.
  63. %%%
  64.  
  65. %%% A list of settings.
  66.      choice :-
  67.     infinity(X),
  68.     write_line(2,'Default settings:'),
  69.     write_line(5,'clause_generation_loop.'),
  70.     write_line(5,'count_all_literals.'),
  71.     write_line(5,'depth_coef(0).'),
  72.     write_line(5,'do_hyper_linking.'),
  73.     write_line(5,'duplicate_partial_instance_test.'),
  74.     write_line(5,'fast_priority_update.'),
  75.     write_line(5,'greatest_time_bound(800).'),
  76.     write_line(5,'hl_literal_reordering.'),
  77.     write_line(5,'least_time_bound(200).'),
  78.     write_line(5,'literal_coef(0).'),
  79.     write_line(5,'max_no_clauses(1600).'),
  80.     write_line(5,'precompute_constraints.'),
  81.     write_line(5,'relevance_bound(',X,').'),
  82.     write_line(5,'relevance_coef(0).'),
  83.     write_line(5,'replace_literal_reordering.'),
  84.     write_line(5,'restricted_equality_transform(X).'),
  85.     write_line(5,'restricted_rewrite.'),
  86.     write_line(5,'safe_early_priority_test.'),
  87.     write_line(5,'save_rewrite_rules.'),
  88.     write_line(5,'save_unrestricted_normal_form.'),
  89.         write_line(5,'simple_small_proof_check.'),
  90.     write_line(5,'size_coef(1).'),
  91.     write_line(5,'small_proof_check.'),
  92.     write_line(5,'small_proof_nucleus_bound(',X,').'),
  93.     write_line(5,'small_proof_size_bound(',X,').'),
  94.     write_line(5,'spc_literal_reordering.'),
  95.     write_line(5,'start_no_clauses_coef(3).'),
  96.     write_line(5,'support_list([b,f]).'),
  97.     write_line(5,'tautology_deletion.'),
  98.         write_line(5,'term_ordering(lpo).'),
  99.     write_line(5,'time_limit(2000).'),
  100.     write_line(5,'unit_resolution.'),
  101.     write_line(5,'user_control.'),
  102.     write_line(2,'more (y./n.)?'),
  103.     read(Step1),
  104.     choice2(Step1).
  105.  
  106.      choice2(y) :-
  107.     write_line(2,'print-out commands(set/clear):'),
  108.     write_line(5,'outCacg: print out clauses after clause generation'),
  109.     write_line(5,'outCagen: print out clauses after generation'),
  110.     write_line(5,'outCahl: print out clauses after hyper-linking'),
  111.     write_line(5,'outCainst: print out clauses after instance deletion.'),
  112.     write_line(5,'outCasimp: print out clauses after subsump/simplif.'),
  113.     write_line(5,'outcsplit: print out results of clause splitting.'),
  114.     write_line(5,'outfls: compute real fully linked subset.'),
  115.     write_line(5,'outinst: print out nucleus and hyper-instances.'),
  116.     write_line(5,'outhllits: print out literal lists for hyper-linking.'),
  117.     write_line(5,'outpc: print out model or relevant clauses for PC.'),
  118.     write_line(5,'outpcin: print out input set to PC.'),
  119.     write_line(5,'outrwt: print out rewrite rules.'),
  120.     write_line(5,'outrwt: print out rewritten terms.'),
  121.     write_line(5,'outtreq: print out transformed equations.'),
  122.     write_line(2,'more (y./n.)?'),
  123.     read(Step2),
  124.     choice3(Step2), !.
  125.      choice2(n).
  126.  
  127.      choice3(y) :-
  128.     write_line(2,'settings[assign(name,value)/delete(name,arity)]:'),
  129.     write_line(5,'clause_splitting(N): maximum size of clause after clause splitting.'),
  130.     write_line(5,'depth_coef(D): depth coefficient for priority.'),
  131.     write_line(5,'literal_coef(L): depth coefficient for priority.'),
  132.     write_line(5,'max_no_clauses(M): max number of clauses retained.'),
  133.     write_line(5,'relevance_bound(R): relevance bound for clauses.'),
  134.     write_line(5,'relevance_coef(R): depth coefficient for priority.'),
  135.     write_line(5,'restricted_equality_transform(N): use restricted equality transform if equality transform generates clause with more than N literals.'),
  136.     write_line(5,'size_coef(S): depth coefficient for priority.'),
  137.     write_line(5,'start_no_clauses(S): starting number of clauses retained.'),
  138.     write_line(5,'start_no_clauses_coef(S): factor to multiply start_no_clauses.'),
  139.     write_line(5,'support_list(S): support strategies.'),
  140.     write_line(5,'term_ordering(O): term ordering.'),
  141.     write_line(5,'time_limit(M): time limit for a run.'),
  142.     write_line(5,'time_limit_coef(C): time limit coefficient for a run.'),
  143.     write_line(5,'time_limit_multiple(M): advance time limit by M times for supervisor mode.'),
  144.     write_line(2,'more (y./n.)?'),
  145.     read(Step3),
  146.     choice4(Step3), !.
  147.      choice3(n).
  148.  
  149.      choice4(y) :-
  150.     write_line(2,'settings[assign(name,value)/delete(name,arity)]:'),
  151.     write_line(5,'back_literalbound(B): literal bound of number of literals for a backward supported clause.'),
  152.     write_line(5,'small_proof_nucleus_bound(N): maximum number of literals in nucleus during small proof checking.'),
  153.     write_line(5,'small_proof_size_bound(D).'),
  154.     write_line(5,'for_literalbound(F): literal bound of number of literals for a forward supported clause.'),
  155.     write_line(5,'literal_bound(L): literal bound of number of literals for a clause.'),
  156.     write_line(5,'user_literalbound(U): literal bound of number of literals for a user supported clause.'),
  157.     write_line(5,'start_priority_bound(S): starting priority bound for fixed priority.'),
  158.     write_line(5,'priority_bound_increment(I): priority bound increment for fixed priority'),
  159.     write_line(5,'start_wu_bound(S): starting work unit bound for sliding priority.'),
  160.         write_line(5,'cache_size(S): maximum size of caches used in constrained rewriting.'),
  161.     write_line(2,'more (y./n.)?'),
  162.     read(Step4),
  163.     choice5(Step4), !.
  164.      choice4(n).
  165.  
  166.      choice5(y) :-
  167.     write_line(2,'options(set/clear):'),
  168.     write_line(5,'auto_orient: generate rewrite rules from equations.'),
  169.     write_line(5,'clause_generation_loop: repeatedly generate clauses after hyper-linking until no new clauses are generated.'),
  170.     write_line(5,'constrained_rewriting: use constrained rewriting.'),
  171.     write_line(5,'count_all_literals: count all literals in the sliding priority computation.'),
  172.     write_line(5,'delete_all_instances: delete all instances.'),
  173.     write_line(5,'delete_nf_instances: delete non-forward supported instances.'),
  174.     write_line(5,'do_hyper_linking: perform hyper-linking.'),
  175.     write_line(5,'duplicate_partial_instance_test: perform duplicate partial instance test.'),
  176.     write_line(5,'early_tautology_test: perform early tautology test.'),
  177.     write_line(5,'early_unit_subsumption: perform early unit subsumption test.'),
  178.     write_line(5,'equality_early_unit_subsumption: perform equality early unit subsumption test.'),
  179.     write_line(5,'equality_transform: perform equality transformation.'),
  180.     write_line(5,'equality_transform_by_round: perform equality transformation at beginning of each round.'),
  181.     write_line(5,'equational_rewrite: use equational rewrite rules.'),
  182.     write_line(5,'fast_priority_update: update sliding priority after each link.'),
  183.     write_line(5,'fixed_priority: use fixed priority.'),
  184.     write_line(5,'ground_disting_after_match: ground distinguished literals after matching for replacements.'),
  185.     write_line(5,'ground_restriction: ground instances for replacements.'),
  186.     write_line(5,'ground_substitution: ground electrons for replacements.'),
  187.     write_line(5,'group_detection: automatically assert group properties.'),
  188.     write_line(5,'hl_literal_reordering: reordering for hyper-linking.'),
  189.     write_line(5,'include_original_clause: include original clause when performing equality transform.'),
  190.     write_line(5,'precompute_constraints: precompute constraints when rewriting a clause with constrained rewriting'),
  191.     write_line(5,'pullout_constants: constants are pulled out when transforming equations'),
  192.     write_line(5,'realfls: compute real largest fully linked subset.'),
  193.     write_line(5,'replace_literal_reordering: reordering for replacement.'),
  194.     write_line(5,'replacement: use definition replacements for literals.'),
  195.     write_line(5,'restricted_rewrite: use restricted rewrite when rewriting equations.'),
  196.     write_line(5,'safe_early_priority_test: perform early priority test so only "safe" partial instances are pruned.'),
  197.     write_line(5,'save_rewrite_rules: save rewrites rules between sessions.'),
  198.     write_line(5,'save_unrestricted_normal_form: save unrestricted normal form under restricted rewriting.'),
  199.     write_line(5,'simple_small_proof_check: use unit clauses as elctrons in small proof check.'),
  200.     write_line(5,'size_by_clause: the clause size for priority is the sum of all literal sizes.'),
  201.     write_line(5,'slidepriority: use sliding priority.'),
  202.     write_line(5,'small_proof_check: call small proof checking.'),
  203.     write_line(5,'small_proof_check_all: use all clauses for nucleus in small proof checking.'),
  204.     write_line(5,'spc_literal_reordering: reordering for small proof.'),
  205.     write_line(5,'sum_of_measures: priority is the sum of measures.'),
  206.     write_line(5,'super_batch: batch mode for top level supervisor.'),
  207.     write_line(5,'tautology_deletion: perform tautology deletion.'),
  208.     write_line(5,'unit_resolution: call unit subsumption/simplification.'),
  209.     write_line(5,'user_control: do not call top level supervisor.'),
  210.     write_line(2,'more (y./n.)?'),
  211.     read(Step5),
  212.     choice6(Step5), !.
  213.      choice5(n).
  214.  
  215.      choice6(y) :-
  216.     write_line(2,'These are for top level supervisor[assign(<name,value)/delete(name,arity)]:'),
  217.     write_line(5,'least_time_bound(B): lower time bound.'),
  218.     write_line(5,'greatest_time_bound(B): upper time bound.'), nl.
  219.      choice6(n).
  220.  
  221. %%% Change options.
  222.      set_clear_comlist([outCacg, outCagen, outCahl, outCainst, outCasimp,
  223.             outcsplit, outfls, outinst, outhllits, outpc, outpcin, 
  224.             outrwr, outrwt, outtreq,
  225.             auto_orient, clause_generation_loop,
  226.             constrained_rewriting,
  227.             count_all_literals, delete_all_instances, 
  228.             delete_nf_instances, do_hyper_linking,
  229.             duplicate_partial_instance_test,
  230.             early_tautology_test, early_unit_subsumption,
  231.             equality_early_unit_subsumption,
  232.             equality_transform, equality_transform_by_round,
  233.             equational_rewrite, fast_priority_update,
  234.             fixed_priority, ground_disting_after_match,
  235.             ground_restriction, ground_substitution,
  236.             group_detection, hl_literal_reordering, 
  237.             include_original_clause, pullout_constants,
  238.             precompute_constraints,    realfls,
  239.             replace_literal_reordering,
  240.             replacement, restricted_rewrite,
  241.             safe_early_priority_test,
  242.             save_rewrite_rules, save_unrestricted_normal_form,
  243.             simple_small_proof_check,
  244.             size_by_clause, slidepriority,
  245.             small_proof_check, small_proof_check_all,
  246.             spc_literal_reordering, sum_of_measures,
  247.             super_batch, tautology_deletion, 
  248.             unit_resolution, user_control]).
  249.  
  250.      assign_delete_comlist([clause_splitting, cache_size, depth_coef,
  251.                 literal_coef, max_no_clauses,
  252.                 relevance_bound, relevance_coef,
  253.                 restricted_equality_transform, size_coef,
  254.                 start_no_clauses, start_no_clauses_coef,
  255.                 support_list, term_ordering, time_limit,
  256.                 time_limit_coef, time_limit_multiple, 
  257.                 back_literalbound, small_proof_nucleus_bound,
  258.                 small_proof_size_bound,
  259.                 for_literalbound, literal_bound,
  260.                 user_literalbound, priority_bound_increment,
  261.                 start_priority_bound,
  262.                 start_wu_bound, least_time_bound,
  263.                 greatest_time_bound]).
  264.  
  265.      set(Command) :- 
  266.     set_clear_comlist(ComList), 
  267.     member(Command, ComList), 
  268.     !, assertin(Command,0,Command).
  269.      set(Command) :- 
  270.     write_line(5, 'No such command: ', Command).
  271.  
  272.      clear(Command) :- 
  273.     set_clear_comlist(ComList), 
  274.     member(Command, ComList),
  275.     !, pullout(Command,0).
  276.      clear(Command) :- 
  277.     write_line(5, 'No such command: ', Command). 
  278.  
  279.      assign_cmd(Command,X) :-
  280.     assign_delete_comlist(ComList), 
  281.     member(Command, ComList),
  282.     Com =.. [Command, X],
  283.     !, assertin(Command,1,Com).
  284.      assign_cmd(Command,_) :-
  285.     write_line(5, 'No such command: ', Command).  
  286.  
  287.      delete(Command,X) :-
  288.     assign_delete_comlist(ComList),    
  289.     member(Command, ComList), 
  290.     !, abolish(Command,X).
  291.      delete(Command,_) :-
  292.     write_line(5, 'No such command: ', Command).
  293.  
  294.      assertin(X,N,Y) :-
  295.     abolish(X,N),
  296.     assert(Y).
  297.  
  298.      pullout(X,N) :-
  299.     abolish(X,N).
  300.  
  301. %%% SET DEFAULTS
  302.      cache_size(1000000).
  303.      clause_generation_loop.
  304.      count_all_literals.
  305.      depth_coef(0).
  306.      do_hyper_linking.
  307.      duplicate_partial_instance_test.
  308.      fast_priority_update.
  309.      greatest_time_bound(800).
  310.      hl_literal_reordering.
  311.      infinity(1000).
  312.      least_time_bound(200).
  313.      literal_coef(0).
  314.      max_no_clauses(1600).
  315.      precompute_constraints.
  316.      relevance_coef(0).
  317.      replace_literal_reordering.
  318.      restricted_rewrite.
  319.      restricted_equality_transform(0).
  320.      safe_early_priority_test.
  321.      save_rewrite_rules.
  322.      save_unrestricted_normal_form.
  323.      simple_small_proof_check.
  324.      size_coef(1).
  325.      small_proof_check.
  326.      spc_literal_reordering.
  327.      start_no_clauses_coef(3).
  328.      support_list([b,f]).
  329.      tautology_deletion.
  330.      term_ordering(lpo).
  331.      time_limit(2000).
  332.      unit_resolution.
  333.      user_control.
  334.      set_infinity_defaults :-
  335.     infinity(X),
  336.     assert(relevance_bound(X)),
  337.     assert(small_proof_nucleus_bound(X)),
  338.     assert(small_proof_size_bound(X)),
  339.     !.
  340.      set_priority_bound_increment_default :-
  341.     fixed_priority,
  342.         not(priority_bound_increment(_)),
  343.     !,
  344.     assert(priority_bound_increment(1)).
  345.      set_priority_bound_increment_default.
  346.  
  347. %%% constant list for transforming clauses or literals to ground.
  348.      const_list(['$1','$2','$3','$4','$5','$6','$7','$8','$9','$10',
  349.          '$11','$12','$13','$14','$15','$16','$17','$18','$19','$20',
  350.          '$21','$22','$23','$24','$25','$26','$27','$28','$29','$30',
  351.          '$31','$32','$33','$34','$35','$36','$37','$38','$39','$40',
  352.          '$41','$42','$43','$44','$45','$46','$47','$48','$49','$50',
  353.          '$51','$52','$53','$54','$55','$56','$57','$58','$59','$60',
  354.          '$61','$62','$63','$64','$65','$66','$67','$68','$69','$70',
  355.          '$71','$72','$73','$74','$75','$76','$77','$78','$79','$80',
  356.          '$81','$82','$83','$84','$85','$86','$87','$88','$89','$90',
  357.          '$91','$92','$93','$94','$95','$96','$97','$98','$99','$100']).
  358.  
  359. %%% constant list for transforming clauses to Gr(F).
  360.      grf_list(['$','$','$','$','$','$','$','$','$','$',
  361.            '$','$','$','$','$','$','$','$','$','$',
  362.            '$','$','$','$','$','$','$','$','$','$',
  363.            '$','$','$','$','$','$','$','$','$','$',
  364.            '$','$','$','$','$','$','$','$','$','$',
  365.            '$','$','$','$','$','$','$','$','$','$',
  366.            '$','$','$','$','$','$','$','$','$','$',
  367.            '$','$','$','$','$','$','$','$','$','$',
  368.            '$','$','$','$','$','$','$','$','$','$',
  369.            '$','$','$','$','$','$','$','$','$','$']).
  370.  
  371. %%% A list of 100 variables. This is for making pretty outputs.
  372.      var_list(['V','W','X','Y','Z', 'V1','W1','X1','Y1','Z1',
  373.           'V2','W2','X2','Y2','Z2', 'V3','W3','X3','Y3','Z3',
  374.           'V4','W4','X4','Y4','Z4', 'V5','W5','X5','Y5','Z5',
  375.           'V6','W6','X6','Y6','Z6', 'V7','W7','X7','Y7','Z7',
  376.           'V8','W8','X8','Y8','Z8', 'V9','W9','X9','Y9','Z9',
  377.           'V10','W10','X10','Y10','Z10', 'V11','W11','X11','Y11','Z11',
  378.           'V12','W12','X12','Y12','Z12', 'V13','W13','X13','Y13','Z13',
  379.           'V14','W14','X14','Y14','Z14', 'V15','W15','X15','Y15','Z15',
  380.           'V16','W16','X16','Y16','Z16', 'V17','W17','X17','Y17','Z17',
  381.           'V18','W18','X18','Y18','Z18', 'V19','W19','X19','Y19','Z19']).
  382.